(set-logic HO_ALL)
(set-info :status unsat)
(set-option :uf-lazy-ll true)
(set-option :fmf-bound true)

(declare-const EMP (Bag (Tuple Int String String Int Int Int Int Int Int)))
(declare-const p0 (-> (Tuple Int String String Int Int Int Int Int Int) Bool))
(declare-const q1 (Bag (Tuple Int String String Int Int Int Int Int Int)))
(declare-const q2 (Bag (Tuple Int String String Int Int Int Int Int Int)))
(declare-const p2 (-> (Tuple Int String String Int Int Int Int Int Int) Bool))
(declare-const p4 (-> (Tuple Int String String Int Int Int Int Int Int) Bool))
(declare-const f10 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(declare-const f12 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(declare-const p7 (-> (Tuple Int String String Int Int Int Int Int Int) Bool))
(declare-const p9 (-> (Tuple Int String String Int Int Int Int Int Int) Bool))
(declare-const f13 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(declare-const f1 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(declare-const f3 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(declare-const f5 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(declare-const f6 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(declare-const p11 (-> (Tuple Int String String Int Int Int Int Int Int) Bool))
(declare-const f8 (-> (Tuple Int String String Int Int Int Int Int Int) (Tuple Int String String Int Int Int Int Int Int)))
(assert (= p0 (lambda ((t (Tuple Int String String Int Int Int Int Int Int)))  (=  ((_ tuple.select 7) t) 10))))
(assert (= f1 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (= p2 (lambda ((t (Tuple Int String String Int Int Int Int Int Int)))  (=  ((_ tuple.select 7) t) 20))))
(assert (= f3 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (= p4 (lambda ((t (Tuple Int String String Int Int Int Int Int Int)))  (=  ((_ tuple.select 7) t) 30))))
(assert (= f5 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (= f6 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (= p7 (lambda ((t (Tuple Int String String Int Int Int Int Int Int)))  (=  ((_ tuple.select 7) t) 10))))
(assert (= f8 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (= p9 (lambda ((t (Tuple Int String String Int Int Int Int Int Int)))  (=  ((_ tuple.select 7) t) 20))))
(assert (= f10 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (= p11 (lambda ((t (Tuple Int String String Int Int Int Int Int Int)))  (=  ((_ tuple.select 7) t) 30))))
(assert (= f12 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (not (= q1 q2)))
(assert (= f13 (lambda ((t (Tuple Int String String Int Int Int Int Int Int))) (tuple ((_ tuple.select 0) t) ((_ tuple.select 1) t) ((_ tuple.select 2) t) ((_ tuple.select 3) t) ((_ tuple.select 4) t) ((_ tuple.select 5) t) ((_ tuple.select 6) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
(assert (= q1 (bag.difference_remove (bag.map f1 (bag.filter p0 EMP)) (bag.map f6 (bag.difference_remove (bag.map f3 (bag.filter p2 EMP)) (bag.map f5 (bag.filter p4 EMP)))))))
(assert (= q2 (bag.difference_remove (bag.map f8 (bag.filter p7 EMP)) (bag.map f13 (bag.difference_remove (bag.map f10 (bag.filter p9 EMP)) (bag.map f12 (bag.filter p11 EMP)))))))
(check-sat)
